k:Knd. isrcv(k)  lnk(k)  IdLnk 

latex

Definitions	Knd, isrcv(k), lnk(k), 1of(t), x. t(x), outl(x), P  Q, b, isl(x), x:A. B(x), IdLnk, t  T, Id
Lemmas	Id wf, IdLnk wf, isl wf, assert wf, outl wf, pi1 wf